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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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: 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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
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₁ b ∨ a_2 = in₂ c ∨ 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: 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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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: 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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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₁ 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₁ b ∨ a_2 = in₂ c ∨ 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: 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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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₁ b → ¬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
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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₁ b → ¬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₀ 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₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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₁ b → ¬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₀ 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₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₄ h₂₅ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₂₆ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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₁ b → ¬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₀ 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₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₄ h₂₅ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
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₁ b ∨ a_2 = in₂ c ∨ 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: 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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → 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₀ a_1 → 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₂ c → 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₁ b → ¬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₀ 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₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₄ h₂₅ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₁ b → ¬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₃₀ 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₁ b ∨ a_2 = in₂ c ∨ 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: 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_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1 → 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 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1 → 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₂ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_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
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ 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₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
have h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
Tactic: try tauto