awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
huv : Forall₂ r [] v
nil : (Forall₂ r ∘r Perm) [] []
⊢ (Forall₂ r ∘r Perm) [] v

Tactic:
cases huv
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []

Tactic:
⟨[], Forall₂.nil, Perm.nil⟩

Premises used: List.Forall₂.nil, Relation.Comp, And.intro, Exists.intro, List.Perm.nil, List.nil
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []

Tactic:
exact ⟨[], Forall₂.nil, Perm.nil⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u_1 : List α
u : α
l₁ l₂ : List α
_hlu : l₁ ~ l₂
ih : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v
v : List β
huv : Forall₂ r (u :: l₂) v
cons : ∀ {b : β} {l₂_1 : List β} (hab : r u b) (huv' : Forall₂ r l₂ l₂_1), (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_1)
⊢ (Forall₂ r ∘r Perm) (u :: l₁) v

Tactic:
obtain - | ⟨hab, huv'⟩ := huv
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u_1 : List α
u : α
l₁ l₂ : List α
_hlu : l₁ ~ l₂
ih : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v
b : β
l₂_1 : List β
hab : r u b
huv' : Forall₂ r l₂ l₂_1
cons : ∀ (l₂ : List β) (h₁₂ : Forall₂ r l₁ l₂) (h₂₃ : l₂ ~ l₂_1), (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_1)
⊢ (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_1)

Tactic:
rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u_1 : List α
u : α
l₁ l₂_1 : List α
_hlu : l₁ ~ l₂_1
ih : ∀ {v : List β} (huv : Forall₂ r l₂_1 v), (Forall₂ r ∘r Perm) l₁ v
b : β
l₂_2 : List β
hab : r u b
huv' : Forall₂ r l₂_1 l₂_2
l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₂_2
⊢ (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_2)

Tactic:
⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩

Premises used: List.Forall₂.cons, List.Perm.cons, List.cons, Relation.Comp, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u_1 : List α
u : α
l₁ l₂_1 : List α
_hlu : l₁ ~ l₂_1
ih : ∀ {v : List β} (huv : Forall₂ r l₂_1 v), (Forall₂ r ∘r Perm) l₁ v
b : β
l₂_2 : List β
hab : r u b
huv' : Forall₂ r l₂_1 l₂_2
l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₂_2
⊢ (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_2)

Tactic:
exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
v : List β
huv : Forall₂ r (a₁ :: a₂ :: h₂₃) v
swap :
  ∀ {b : β} {l₂ : List β} (h₁ : r a₁ b) (hr₂₃ : Forall₂ r (a₂ :: h₂₃) l₂),
    (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: l₂)
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) v

Tactic:
obtain - | ⟨h₁, hr₂₃⟩ := huv
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b : β
l₂ : List β
h₁ : r a₁ b
hr₂₃ : Forall₂ r (a₂ :: h₂₃) l₂
swap :
  ∀ {b_1 : β} {l₂ : List β} (h₂ : r a₂ b_1) (h₁₂ : Forall₂ r h₂₃ l₂),
    (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: b_1 :: l₂)
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: l₂)

Tactic:
obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b : β
h₁ : r a₁ b
b_1 : β
l₂ : List β
h₂ : r a₂ b_1
h₁₂ : Forall₂ r h₂₃ l₂
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: b_1 :: l₂)

Tactic:
⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩

Premises used: List.Forall₂.cons, List.Perm.swap, Relation.Comp, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b : β
h₁ : r a₁ b
b_1 : β
l₂ : List β
h₂ : r a₂ b_1
h₁₂ : Forall₂ r h₂₃ l₂
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: b_1 :: l₂)

Tactic:
exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
ih₁ : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v
ih₂ : ∀ {v : List β} (huv : Forall₂ r l₃ v), (Forall₂ r ∘r Perm) l₂ v
v : List β
huv : Forall₂ r l₃ v
trans : ∀ (lb₂ : List β) (hab₂ : Forall₂ r l₂ lb₂) (h₂₃ : lb₂ ~ v), (Forall₂ r ∘r Perm) l₁ v
⊢ (Forall₂ r ∘r Perm) l₁ v

Tactic:
rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
ih₁ : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v
ih₂ : ∀ {v : List β} (huv : Forall₂ r l₃ v), (Forall₂ r ∘r Perm) l₂ v
v : List β
huv : Forall₂ r l₃ v
lb₂ : List β
hab₂ : Forall₂ r l₂ lb₂
h₂₃ : lb₂ ~ v
trans : ∀ (lb₁ : List β) (hab₁ : Forall₂ r l₁ lb₁) (h₁₂ : lb₁ ~ lb₂), (Forall₂ r ∘r Perm) l₁ v
⊢ (Forall₂ r ∘r Perm) l₁ v

Tactic:
rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
ih₁ : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v
ih₂ : ∀ {v : List β} (huv : Forall₂ r l₃ v), (Forall₂ r ∘r Perm) l₂ v
v : List β
huv : Forall₂ r l₃ v
lb₂ : List β
hab₂ : Forall₂ r l₂ lb₂
h₂₃ : lb₂ ~ v
lb₁ : List β
hab₁ : Forall₂ r l₁ lb₁
h₁₂ : lb₁ ~ lb₂
⊢ (Forall₂ r ∘r Perm) l₁ v

Tactic:
⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩

Premises used: List.Perm.trans, Relation.Comp, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
ih₁ : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v
ih₂ : ∀ {v : List β} (huv : Forall₂ r l₃ v), (Forall₂ r ∘r Perm) l₂ v
v : List β
huv : Forall₂ r l₃ v
lb₂ : List β
hab₂ : Forall₂ r l₂ lb₂
h₂₃ : lb₂ ~ v
lb₁ : List β
hab₁ : Forall₂ r l₁ lb₁
h₁₂ : lb₁ ~ lb₂
⊢ (Forall₂ r ∘r Perm) l₁ v

Tactic:
exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
hlu : l ~ u
huv : Forall₂ r u v
nil : ∀ {v : List β} (huv : Forall₂ r [] v), (Forall₂ r ∘r Perm) [] v
cons :
  ∀ (u : α) {l₁ l₂ : List α} (_hlu : l₁ ~ l₂) (ih : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v)
    {v : List β} (huv : Forall₂ r (u :: l₂) v), (Forall₂ r ∘r Perm) (u :: l₁) v
swap :
  ∀ (a₁ a₂ : α) (h₂₃ : List α) {v : List β} (huv : Forall₂ r (a₁ :: a₂ :: h₂₃) v),
    (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) v
trans :
  ∀ {l₁ l₂ l₃ : List α},
    l₁ ~ l₂ →
      l₂ ~ l₃ →
        ∀ (ih₁ : ∀ {v : List β} (huv : Forall₂ r l₂ v), (Forall₂ r ∘r Perm) l₁ v)
          (ih₂ : ∀ {v : List β} (huv : Forall₂ r l₃ v), (Forall₂ r ∘r Perm) l₂ v) {v : List β} (huv : Forall₂ r l₃ v),
          (Forall₂ r ∘r Perm) l₁ v
⊢ (Forall₂ r ∘r Perm) l v

Tactic:
induction hlu generalizing v with
  | nil => cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩
  | cons u _hlu ih =>
    obtain - | ⟨hab, huv'⟩ := huv
    rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
    exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩
  | swap a₁ a₂ h₂₃ =>
    obtain - | ⟨h₁, hr₂₃⟩ := huv
    obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
    exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩
  | trans _ _ ih₁ ih₂ =>
    rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
    rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
    exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩

Premises used: List.Perm.swap, List.cons, List.nil
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
h : ∀ (l₁ : List α) (l₃ : List β), (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r

Tactic:
funext l₁ l₃
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
apply propext

Premises used: propext
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃
h₁ : (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
constructor
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃
h₁ : ∀ (l₂ : List β) (h₁₂ : Forall₂ r l₁ l₂) (h₂₃ : l₂ ~ l₃), (Perm ∘r Forall₂ r) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
rcases h with ⟨l₂, h₁₂, h₂₃⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ Forall₂ (flip r) l₂ l₁

Tactic:
have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
h : ∀ (l' : List α) (h₁ : Forall₂ (flip r) l₃ l') (h₂ : l' ~ l₁), (Perm ∘r Forall₂ r) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩

Premises used: List.perm_comp_forall₂, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
l' : List α
h₁ : Forall₂ (flip r) l₃ l'
h₂ : l' ~ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
⟨l', h₂.symm, h₁.flip⟩

Premises used: List.Forall₂.flip, Relation.Comp, And.intro, Exists.intro, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
l' : List α
h₁ : Forall₂ (flip r) l₃ l'
h₂ : l' ~ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
exact ⟨l', h₂.symm, h₁.flip⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Tactic:
fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃

Premises used: List.perm_comp_forall₂, List.Perm, Relation.Comp, List.Forall₂, _private.0.List.forall₂_comp_perm_eq_perm_comp_forall₂.match_1
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Tactic:
exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : Perm ∘r fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2
| fun (x1 : List β) (x2 : List α) ↦ x1 ~ map f x2

Tactic:
rw [← Relation.comp_eq_fun (map f)]

Premises used: List.map, Relation.comp_eq_fun
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
conv_rhs :
  Eq (α := (a : List β) → (c : List α) → Prop)
    ((fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2) ∘r fun (x1 x2 : List α) ↦ x1 ~ x2)
    (Perm ∘r fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2)
⊢ Eq (α := (a : List β) → (c : List α) → Prop)
    ((fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2) ∘r fun (x1 x2 : List α) ↦ x1 ~ x2)
    fun (x1 : List β) (x2 : List α) ↦ x1 ~ map f x2

Tactic:
conv_rhs => rw [← Relation.comp_eq_fun (map f)]

Premises used: List.map, Relation.comp_eq_fun
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Eq (α := (a : List β) → (c : List α) → Prop)
    ((fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2) ∘r fun (x1 x2 : List α) ↦ x1 ~ x2)
    (Perm ∘r fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2)

Tactic:
simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]

Premises used: List.forall₂_map_right_iff, List.forall₂_comp_perm_eq_perm_comp_forall₂, List.forall₂_eq_eq_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d
rwa : ∀ (this : (flip (Forall₂ r) ∘r Forall₂ r ∘r Perm) b d), ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d), ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← Relation.comp_assoc] at this

Premises used: List.forall₂_comp_perm_eq_perm_comp_forall₂, Relation.comp_assoc
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
hr : BiUnique r
⊢ (Forall₂ r ⇒ Forall₂ r ⇒ fun (x1 x2 : Prop) ↦ x1 ↔ x2) Perm Perm

Tactic:
fun _a _b hab _c _d hcd =>
  Iff.intro (rel_perm_imp hr.2 hab hcd) (rel_perm_imp hr.left.flip hab.flip hcd.flip)

Premises used: List.Forall₂.flip, And.right, And.left, Relator.LeftUnique.flip, Iff.intro, List.rel_perm_imp, Relator.LiftFun
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
P : α → Prop
inst_1 : DecidablePred P
l : List α
a : α
⊢ countP (fun (x : α) ↦ x == a) l =
    countP (fun (x : α) ↦ x == a) (filter (fun (b : α) ↦ decide (P b)) l) +
      countP (fun (x : α) ↦ x == a) (filter (fun (a : α) ↦ !decide (P a)) l)

Tactic:
countP_eq_countP_filter_add l _ P

Premises used: List.countP_eq_countP_filter_add, Decidable.decide
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
P : α → Prop
inst_1 : DecidablePred P
l : List α
a : α
h : ∀ (x : α), (decide ¬P x) = !decide (P x)
⊢ count a l = count a (filter (fun (b : α) ↦ decide (P b)) l) + count a (filter (fun (x : α) ↦ decide ¬P x) l)

Tactic:
convert! countP_eq_countP_filter_add l _ P

Premises used: List.countP_eq_countP_filter_add, Decidable.decide
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
P : α → Prop
inst_1 : DecidablePred P
l : List α
a x : α
⊢ (decide ¬P x) = !decide (P x)

Tactic:
simp only [decide_not]

Premises used: decide_not
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : β → α → β
l₁ l₂ : List α
rcomm : RightCommutative f
p : l₁ ~ l₂
⊢ ∀ (b : β), foldl f b l₁ = foldl f b l₂

Tactic:
p.foldl_eq' fun x _hx y _hy z => rcomm.right_comm z x y

Premises used: List.Perm.foldl_eq', RightCommutative.right_comm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
b : β
⊢ foldr f b [] = foldr f b []

Tactic:
rfl
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
r : ∀ (b : β), foldr f b l₁_1 = foldr f b l₂_1
b : β
⊢ foldr f b (x :: l₁_1) = foldr f b (x :: l₂_1)

Tactic:
simp [r b]
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x y : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
r : ∀ (b : β), foldr f b l₁_1 = foldr f b l₂_1
b : β
swap' : f y (f x (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))
⊢ foldr f b (y :: x :: l₁_1) = foldr f b (x :: y :: l₂_1)

Tactic:
simp only [foldr_cons]

Premises used: List.foldr_cons
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x y : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
r : ∀ (b : β), foldr f b l₁_1 = foldr f b l₂_1
b : β
swap' : f x (f y (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))
swap'₁ swap'₂ : f x (f y (foldr f b l₂_1)) = f x (f y (foldr f b l₂_1))
⊢ f y (f x (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))

Tactic:
rw [lcomm.left_comm, r b]

Premises used: LeftCommutative.left_comm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
l₁_1 l₂_1 l₃ : List α
h₁ : l₁_1 ~ l₂_1
h₂ : l₂_1 ~ l₃
r₁ : ∀ (b : β), foldr f b l₁_1 = foldr f b l₂_1
r₂ : ∀ (b : β), foldr f b l₂_1 = foldr f b l₃
b : β
⊢ foldr f b l₁_1 = foldr f b l₃

Tactic:
Eq.trans (r₁ b) (r₂ b)

Premises used: Eq.trans
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
l₁_1 l₂_1 l₃ : List α
h₁ : l₁_1 ~ l₂_1
h₂ : l₂_1 ~ l₃
r₁ : ∀ (b : β), foldr f b l₁_1 = foldr f b l₂_1
r₂ : ∀ (b : β), foldr f b l₂_1 = foldr f b l₃
b : β
⊢ foldr f b l₁_1 = foldr f b l₃

Tactic:
exact Eq.trans (r₁ b) (r₂ b)

Premises used: Eq.trans
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
b : β
nil : ∀ (b : β), foldr f b [] = foldr f b []
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (r : ∀ (b : β), foldr f b l₁ = foldr f b l₂) (b : β), foldr f b (x :: l₁) = foldr f b (x :: l₂)
swap' :
  ∀ (x y : α) {l₁ l₂ : List α},
    l₁ ~ l₂ →
      ∀ (r : ∀ (b : β), foldr f b l₁ = foldr f b l₂) (b : β), foldr f b (y :: x :: l₁) = foldr f b (x :: y :: l₂)
trans :
  ∀ {l₁ l₂ l₃ : List α},
    l₁ ~ l₂ →
      l₂ ~ l₃ →
        ∀ (r₁ : ∀ (b : β), foldr f b l₁ = foldr f b l₂) (r₂ : ∀ (b : β), foldr f b l₂ = foldr f b l₃) (b : β),
          foldr f b l₁ = foldr f b l₃
⊢ foldr f b l₁ = foldr f b l₂

Tactic:
induction p using Perm.recOnSwap' generalizing b with
  | nil => rfl
  | cons _ _ r => simp [r b]
  | swap' _ _ _ r => simp only [foldr_cons]; rw [lcomm.left_comm, r b]
  | trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b)

Premises used: List.foldr_cons, List.Perm.cons, LeftCommutative.left_comm, List.Perm.trans, List.Perm.swap', List.Perm.nil
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
op : α → α → α
IA : Std.Associative op
IC : Std.Commutative op
l₁ l₂ : List α
a : α
h : l₁ ~ l₂
⊢ (l₁ <*> a) = l₂ <*> a

Tactic:
h.foldl_eq _

Premises used: List.Perm.foldl_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
op : α → α → α
IA : Std.Associative op
IC : Std.Commutative op
l₁ l₂ : List α
a : α
h : l₁ ~ l₂
⊢ foldr op a l₁ = foldr op a l₂

Tactic:
h.foldr_eq _

Premises used: List.Perm.foldr_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
o₁ o₂ : Option α
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂

Tactic:
⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩

Premises used: Option.toList, Eq.rec, List.Perm.refl, Iff.intro
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
o₁ o₂ : Option α
refine : ∀ (p : o₁.toList ~ o₂.toList), o₁ = o₂
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂

Tactic:
refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
none : ∀ (p : Option.toList Option.none ~ o₂.toList), Option.none = o₂
some : ∀ (a : α) (p : (Option.some a).toList ~ o₂.toList), Option.some a = o₂
⊢ o₁ = o₂

Tactic:
rcases o₁ with - | a
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
o₂ : Option α
p : Option.toList Option.none ~ o₂.toList
none :
  ∀ (p : Perm.{u_1} (α := α) (Option.toList Option.none) (Option.toList Option.none)),
    Eq.{u_1 + 1} (α := Option α) Option.none Option.none
none₁ : ∀ (b : α) (p : Option.toList Option.none ~ (some b).toList), Option.none = some b
⊢ Option.none = o₂

Tactic:
rcases o₂ with - | b
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
o₂ : Option α
a : α
p : (Option.some a).toList ~ o₂.toList
some : ∀ (p : (Option.some a).toList ~ Option.toList none), Option.some a = none
some₁ : ∀ (b : α) (p : (Option.some a).toList ~ (Option.some b).toList), Option.some a = Option.some b
⊢ Option.some a = o₂

Tactic:
rcases o₂ with - | b
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
p : Perm.{u_1} (α := α) (Option.toList none) (Option.toList none)
⊢ Eq.{u_1 + 1} (α := Option α) none none

Tactic:
rfl
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
b : α
p : Option.toList none ~ (some b).toList
⊢ none = some b

Tactic:
cases p.length_eq

Premises used: List.Perm.length_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a : α
p : (some a).toList ~ Option.toList none
⊢ some a = none

Tactic:
cases p.length_eq

Premises used: List.Perm.length_eq
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ b ∈ (some b).toList

Tactic:
simp
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b

Tactic:
exact Option.mem_toList.1 (p.symm.subset <| by simp)

Premises used: Option.mem_toList, List.Perm.subset, Iff.mp, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
rw :
  (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]

Premises used: List.perm_iff_count, Decidable.and_forall_ne
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
this : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]

Premises used: List.count_replicate, Ne.symm, List.count_eq_zero
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
suffices : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
    simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
trans : l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a
trans₁ : (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
trans ∀ c, c ∈ l → c = b ∨ c = a
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

Tactic:
simp [subset_def, or_comm]

Premises used: List.subset_def, or_comm
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x : α
rw : x ∈ l → x = b ∨ x = a ↔ x ≠ b ∧ x ≠ a → ¬x ∈ l
rw₁ : x ∈ l → x = b ∨ x = a ↔ ¬(x = b ∨ x = a) → ¬x ∈ l
rw₂ rw₃ : x ∈ l → x = b ∨ x = a ↔ x ∈ l → x = b ∨ x = a
⊢ x ∈ l → x = b ∨ x = a ↔ x ≠ b → x ≠ a → ¬x ∈ l

Tactic:
rw [← and_imp, ← not_or, not_imp_not]

Premises used: and_imp, not_or, not_imp_not
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]

Premises used: forall_congr'
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
rw rw₁ : map f l ~ map f l' ↔ (fun (x1 : List β) (x2 : List α) ↦ x1 ~ map f x2) (map f l) l'
⊢ map f l ~ map f l' ↔
    Relation.Comp (fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2) (fun (x1 x2 : List α) ↦ x1 ~ x2) (map f l) l'

Tactic:
rw [eq_map_comp_perm]

Premises used: List.eq_map_comp_perm