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 (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₀ (a, b, c).1)
have a₁ : ((a, b, c).1, b, (a, b, c).2.2) ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : 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)
have a₁ : (a, (a, b, c).2.1, (a, b, c).2.2) ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : 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)
have a₁ : (a, (a, b, c).2.1, (a, b, c).2.2) ∈ t
Tactic: constructor
-- 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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
⊢ Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} {in₀ a, in₁ b, in₂ c_1}
have h : ∀ (a_2 : α ⊕ β ⊕ γ),
  Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2 ↔
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2
Tactic: ext
-- 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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2 ↔
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2
have h : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton]
-- 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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₁₀ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₀ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₁ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₂ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₃ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₄ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₅ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₆ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₇ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₉ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₀ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₁ h₂₂ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₂₃ : a_2 = in₁ b → ¬a_2 = in₀ a → ¬a_2 = in₁ b → a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₀ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₁ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₂ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₃ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₄ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₅ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₆ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₇ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₉ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₀ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₁ h₂₂ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₀ a → ¬a_2 = in₁ b → a_2 = in₂ c_1
h₂₄ h₂₅ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₂₆ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → ¬a_2 = in₁ b → a_2 = in₂ c_1
Tactic: 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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₁₀ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₀ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₁ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₂ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₃ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₄ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₅ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₆ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₇ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₉ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₀ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₁ h₂₂ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₂₃ : a_2 = in₁ b → ¬a_2 = in₀ a → ¬a_2 = in₁ b → a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h h₁ : a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₃ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₄ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₆ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₇ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₉ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₀ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₁ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₂ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₃ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₄ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₅ : a_2 = in₁ b → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₆ : a_2 = in₂ c_1 → a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₇ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₁₉ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₀ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₁ h₂₂ : a_2 = in₁ b → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₀ a → ¬a_2 = in₁ b → a_2 = in₂ c_1
h₂₄ h₂₅ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → a_2 = in₁ b ∨ a_2 = in₂ c_1
⊢ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1 ↔ a_2 = in₀ a ∨ a_2 = in₁ b ∨ a_2 = in₂ c_1
have h₂₆ : a_2 = in₂ c_1 → ¬a_2 = in₀ a → ¬a_2 = in₁ b → a_2 = in₂ c_1
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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
⊢ ∃ (a_2 : α) (b_2 : β) (c : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a_2, in₁ b_2, in₂ c} {in₀ a, in₁ b, in₂ c_1} ∧
      (graph t).Adj (in₀ a_2) (in₁ b_2) ∧ (graph t).Adj (in₀ a_2) (in₂ c) ∧ (graph t).Adj (in₁ b_2) (in₂ c)
have in₀₁ : (graph t).Adj (in₀ a) (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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
in₀₁ : (graph t).Adj (in₀ a) (in₁ b)
⊢ ∃ (a_2 : α) (b_2 : β) (c : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a_2, in₁ b_2, in₂ c} {in₀ a, in₁ b, in₂ c_1} ∧
      (graph t).Adj (in₀ a_2) (in₁ b_2) ∧ (graph t).Adj (in₀ a_2) (in₂ c) ∧ (graph t).Adj (in₁ b_2) (in₂ c)
have in₂ : (graph t).Adj (in₀ a) (in₂ c_1)
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
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
in₀₁ : (graph t).Adj (in₀ a) (in₁ b)
in₂ : (graph t).Adj (in₀ a) (Sum3.in₂ c_1)
⊢ ∃ (a_2 : α) (b_2 : β) (c : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a_2, in₁ b_2, Sum3.in₂ c} {in₀ a, in₁ b, Sum3.in₂ c_1} ∧
      (graph t).Adj (in₀ a_2) (in₁ b_2) ∧ (graph t).Adj (in₀ a_2) (Sum3.in₂ c) ∧ (graph t).Adj (in₁ b_2) (Sum3.in₂ c)
have in₃ : (graph t).Adj (in₁ b) (Sum3.in₂ c_1)
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 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 : (a, b_1, c_1) ∈ t
⊢ Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} {in₁ b, in₀ a, in₂ c_1}
have h : ∀ (a_2 : α ⊕ β ⊕ γ),
  Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2 ↔
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₁ b, in₀ a, in₂ c_1} a_2
Tactic: ext