awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl₅ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → a₁ = b₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
inl₅ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → a₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl₆ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → b₁ = a₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
inl₅ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → a₁ = b₂
inl₆ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → b₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl₇ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → b₁ = a₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
inl₅ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → a₁ = b₂
inl₆ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → b₁ = a₂
inl₇ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → b₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inr₄ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
inl₅ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → a₁ = b₂
inl₆ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → b₁ = a₂
inl₇ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → b₁ = a₂
inr₄ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inr₅ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬b₁ = b₂ → a₁ = b₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ [a₁, b₁].Perm [a₂, b₂]
have rw : [a₂, b₁].Perm [a₂, b₂]
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
rw : [a₂, b₁].Perm [a₂, b₂]
⊢ [a₁, b₁].Perm [a₂, b₂]
have rw₁ : [a₂, b₂].Perm [a₂, b₂]
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁].Perm [a₂, b₂]
have rw : [b₂, a₂].Perm [a₂, b₂]
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x y : α
⊢ (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (x, y))
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (x, y))
have refl : [(x, y).2].Perm [(x, y).2]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x y : α
⊢ (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (x, y))
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (y, x))
have swap : List.Perm.{u_1} (α := α) [] []
Tactic: apply List.Perm.swap'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : List α
hx : x.length = 2
y : List α
hy : y.length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx) (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have nil : ∀ (hx : List.length.{u_1} (α := α) [] = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : List α
hx : x.length = 2
y : List α
hy : y.length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx) (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
nil :
  ∀ (hx : List.length.{u_1} (α := α) [] = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons : ∀ (head : α) (x : List α) (hx : (head :: x).length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head : α
x : List α
hx : (head :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons : ∀ (hx : [head].length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head : α
x : List α
hx : (head :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons :
  ∀ (hx : [head].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons₁ : ∀ (head_1 : α) (x : List α) (hx : (head :: head_1 :: x).length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 : α
x : List α
hx : (head :: head_1 :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons : ∀ (hx : [head, head_1].length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 : α
x : List α
hx : (head :: head_1 :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons :
  ∀ (hx : [head, head_1].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons₁ : ∀ (head_2 : α) (x : List α) (hx : (head :: head_1 :: head_2 :: x).length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 head_2 : α
x : List α
hx : (head :: head_1 :: head_2 :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 : α
hx : [head, head_1].length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons : ∀ (hy : List.length.{u_1} (α := α) [] = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy))
Tactic: rcases y with - | ⟨_, y⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 : α
hx : [head, head_1].length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons :
  ∀ (hy : List.length.{u_1} (α := α) [] = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
have cons₁ : ∀ (head_2 : α) (y : List α) (hy : (head_2 :: y).length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy))
Tactic: rcases y with - | ⟨_, y⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 : α
y : List α
hy : (head_2 :: y).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy))
have cons : ∀ (hy : [head_2].length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy))
Tactic: rcases y with - | ⟨_, y⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 : α
y : List α
hy : (head_2 :: y).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy)
cons :
  ∀ (hy : [head_2].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy))
have cons₁ : ∀ (head_3 : α) (y : List α) (hy : (head_2 :: head_3 :: y).length = 2)
  (h :
    (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: y) hy)),
  Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: y) hy))
Tactic: rcases y with - | ⟨_, y⟩
Cleared hypotheses: y, hy, h