awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
a c : List α
h : (Perm ∘r Perm) a c → a ~ c
⊢ (Perm ∘r Perm) a c ↔ a ~ c
have h₁ : a ~ c → (Perm ∘r Perm) a c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
huv : Forall₂ r [] v
⊢ (Forall₂ r ∘r Perm) [] v
have nil : (Forall₂ r ∘r Perm) [] []
Tactic: cases huv
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) (u :: l₁) v
have cons : ∀ {b : β} {l₂_1 : List β} (hab : r u b) (huv' : Forall₂ r l₂ l₂_1), (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_1)
Tactic: obtain - | ⟨hab, huv'⟩ := huv
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_1)
have cons : ∀ (l₂ : List β) (h₁₂ : Forall₂ r l₁ l₂) (h₂₃ : l₂ ~ l₂_1), (Forall₂ r ∘r Perm) (u :: l₁) (b :: l₂_1)
Tactic: rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) v
have swap : ∀ {b : β} {l₂ : List β} (h₁ : r a₁ b) (hr₂₃ : Forall₂ r (a₂ :: h₂₃) l₂), (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: l₂)
Tactic: obtain - | ⟨h₁, hr₂₃⟩ := huv
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b :: l₂)
have 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₂)
Tactic: obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
Cleared hypotheses: l₂, hr₂₃
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) l₁ v
have trans : ∀ (lb₂ : List β) (hab₂ : Forall₂ r l₂ lb₂) (h₂₃ : lb₂ ~ v), (Forall₂ r ∘r Perm) l₁ v
Tactic: rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) l₁ v
have trans : ∀ (lb₁ : List β) (hab₁ : Forall₂ r l₁ lb₁) (h₁₂ : lb₁ ~ lb₂), (Forall₂ r ∘r Perm) l₁ v
Tactic: rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
hlu : l ~ u
huv : Forall₂ r u v
⊢ (Forall₂ r ∘r Perm) l v
have nil : ∀ {v : List β} (huv : Forall₂ r [] v), (Forall₂ r ∘r Perm) [] 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₂₃⟩
Cleared hypotheses: v, hlu, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) l v
have 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
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₂₃⟩
Cleared hypotheses: v, hlu, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) l v
have swap : ∀ (a₁ a₂ : α) (h₂₃ : List α) {v : List β} (huv : Forall₂ r (a₁ :: a₂ :: h₂₃) v), (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) 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₂₃⟩
Cleared hypotheses: v, hlu, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ (Forall₂ r ∘r Perm) l v
have 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
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₂₃⟩
Cleared hypotheses: v, hlu, huv
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r
have h : ∀ (l₁ : List α) (l₃ : List β), (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
Tactic: funext l₁ l₃
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
have h : (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃
Tactic: apply propext
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃
have h : (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₃
have h₁ : (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₃
have h₁ : ∀ (l₂ : List β) (h₁₂ : Forall₂ r l₁ l₂) (h₂₃ : l₂ ~ l₃), (Perm ∘r Forall₂ r) l₁ l₃
Tactic: rcases h with ⟨l₂, h₁₂, h₂₃⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃
have this : Forall₂ (flip r) l₂ l₁
Tactic: have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃
have h : ∀ (l' : List α) (h₁ : Forall₂ (flip r) l₃ l') (h₂ : l' ~ l₁), (Perm ∘r Forall₂ r) l₁ l₃
Tactic: rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
| fun (x1 : List β) (x2 : List α) ↦ x1 ~ map f x2
have rw : Perm ∘r fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2
Tactic: rw [← Relation.comp_eq_fun (map f)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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)
    fun (x1 : List β) (x2 : List α) ↦ x1 ~ map f x2
have 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)
Tactic: conv_rhs => rw [← Relation.comp_eq_fun (map f)]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
have rwa : ∀ (this : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
have rwa₁ : ∀ (this : ((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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : α → Prop
inst_1 : DecidablePred P
l : List α
a : α
⊢ count a l = count a (filter (fun (b : α) ↦ decide (P b)) l) + count a (filter (fun (x : α) ↦ decide ¬P x) l)
have h : ∀ (x : α), (decide ¬P x) = !decide (P x)
Tactic: convert! countP_eq_countP_filter_add l _ P
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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 : β
⊢ foldr f b (y :: x :: l₁_1) = foldr f b (x :: y :: l₂_1)
have swap' : f y (f x (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))
Tactic: simp only [foldr_cons]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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 : β
⊢ f y (f x (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))
have swap' : f x (f y (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))
Tactic: rw [lcomm.left_comm, r b]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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))
⊢ f y (f x (foldr f b l₁_1)) = f x (f y (foldr f b l₂_1))
have swap'₁ : f x (f y (foldr f b l₂_1)) = f x (f y (foldr f b l₂_1))
Tactic: rw [lcomm.left_comm, r b]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
b : β
⊢ foldr f b l₁ = foldr f b l₂
have nil : ∀ (b : β), foldr f b [] = foldr f b []
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)
Cleared hypotheses: p, b
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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 []
⊢ foldr f b l₁ = foldr f b l₂
have 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₂)
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)
Cleared hypotheses: p, b
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂)
⊢ foldr f b l₁ = foldr f b l₂
have 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₂)
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)
Cleared hypotheses: p, b
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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₂)
⊢ foldr f b l₁ = foldr f b l₂
have 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₃
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)
Cleared hypotheses: p, b
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
o₁ o₂ : Option α
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂
have refine : ∀ (p : o₁.toList ~ o₂.toList), o₁ = o₂
Tactic: refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
⊢ o₁ = o₂
have none : ∀ (p : Option.toList none ~ o₂.toList), none = o₂
Tactic: rcases o₁ with - | a
Cleared hypotheses: o₁, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
none : ∀ (p : Option.toList Option.none ~ o₂.toList), Option.none = o₂
⊢ o₁ = o₂
have some : ∀ (a : α) (p : (some a).toList ~ o₂.toList), some a = o₂
Tactic: rcases o₁ with - | a
Cleared hypotheses: o₁, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
o₂ : Option α
p : Option.toList none ~ o₂.toList
⊢ none = o₂
have none : ∀ (p : Perm.{u_1} (α := α) (Option.toList none) (Option.toList none)), Eq.{u_1 + 1} (α := Option α) none none
Tactic: rcases o₂ with - | b
Cleared hypotheses: o₂, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ Option.none = o₂
have none₁ : ∀ (b : α) (p : Option.toList Option.none ~ (some b).toList), Option.none = some b
Tactic: rcases o₂ with - | b
Cleared hypotheses: o₂, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
o₂ : Option α
a : α
p : (some a).toList ~ o₂.toList
⊢ some a = o₂
have some : ∀ (p : (some a).toList ~ Option.toList none), some a = none
Tactic: rcases o₂ with - | b
Cleared hypotheses: o₂, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ Option.some a = o₂
have some₁ : ∀ (b : α) (p : (Option.some a).toList ~ (Option.some b).toList), Option.some a = Option.some b
Tactic: rcases o₂ with - | b
Cleared hypotheses: o₂, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
have 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]
Tactic: rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (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]
have suffices : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
Tactic: suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
    simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
have trans : l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a
Tactic: trans ∀ c, c ∈ l → c = b ∨ c = a
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
have trans₁ : (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
Tactic: trans ∀ c, c ∈ l → c = b ∨ c = a
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x : α
⊢ x ∈ l → x = b ∨ x = a ↔ x ≠ b → x ≠ a → ¬x ∈ l
have rw : x ∈ l → x = b ∨ x = a ↔ x ≠ b ∧ x ≠ a → ¬x ∈ l
Tactic: rw [← and_imp, ← not_or, not_imp_not]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ x ∈ l → x = b ∨ x = a ↔ x ≠ b → x ≠ a → ¬x ∈ l
have rw₁ : x ∈ l → x = b ∨ x = a ↔ ¬(x = b ∨ x = a) → ¬x ∈ l
Tactic: rw [← and_imp, ← not_or, not_imp_not]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
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
⊢ x ∈ l → x = b ∨ x = a ↔ x ≠ b → x ≠ a → ¬x ∈ l
have rw₂ : x ∈ l → x = b ∨ x = a ↔ x ∈ l → x = b ∨ x = a
Tactic: rw [← and_imp, ← not_or, not_imp_not]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ 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'
have rw : map f l ~ map f l' ↔ (fun (x1 : List β) (x2 : List α) ↦ x1 ~ map f x2) (map f l) l'
Tactic: rw [eq_map_comp_perm]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ Forall₂ (fun (x1 x2 : List β) ↦ x1 ~ x2) (List.map f l) (List.map g l)
have rwa : Forall₂ (fun (a : List β) (c : α) ↦ a ~ g c) (List.map f l) l
Tactic: rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
rwa : Forall₂ (fun (a : List β) (c : α) ↦ a ~ g c) (List.map f l) l
⊢ Forall₂ (fun (x1 x2 : List β) ↦ x1 ~ x2) (List.map f l) (List.map g l)
have rwa₁ : Forall₂ (fun (c b : α) ↦ f c ~ g b) l l
Tactic: rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l
have cons : ∀ (a : α) (l : List α) (IH : flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l),
  flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun (x : α) ↦ f x ++ g x) (a :: l)
Tactic: induction l with | nil => simp | cons a l IH => ?_
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l
⊢ flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun (x : α) ↦ f x ++ g x) (a :: l)
have cons : f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun (x : α) ↦ f x ++ g x) l)
Tactic: simp only [flatMap_cons, append_assoc]