awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
rw₇ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length + 1) * (ts.length + is.length)!
rw₈ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length + 1)
rw₉ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw₁₀ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
rw₁₁ :
  (ts.permutationsAux (t :: is)).length + is.length * is.length ! + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
rw₁₂ :
  (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₁₃ : (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
  (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !)
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw :
  (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
          is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
rw₁ :
  is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₂ :
  is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₃ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
rw₄ :
  is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!
rw₅ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
rw₆ : is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + is.length).succ !
rw₇ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length + 1) * (ts.length + is.length)!
rw₈ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length + 1)
rw₉ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ
rw₁₀ :
  is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
rw₁₁ :
  (ts.permutationsAux (t :: is)).length + is.length * is.length ! + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
rw₁₂ :
  (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
rw₁₃ :
  (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
    (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !)
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
have rw₁₄ : (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !) =
  (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !)
Tactic: rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
⊢ ∀ (ts is l : List α), l ~ is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux is
have refine : ∀ (t : α) (ts is : List α),
  (∀ (l : List α),
      l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
    (∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
      ∀ (l : List α),
        l ~ is ++ t :: ts → (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
Tactic: refine permutationsAux.rec (by simp) ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
have rw : (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
  l ∈ ts.permutationsAux (t :: is) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Tactic: rw [permutationsAux_cons, mem_foldr_permutationsAux2]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
have inl : ∀ (is' : List α) (p' : is' ~ t :: is) (e : l = is' ++ ts),
  (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Tactic: rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
inl :
  ∀ (is' : List α) (p' : is' ~ t :: is) (e : l = is' ++ ts),
    (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
      l ∈ ts.permutationsAux (t :: is) ∨
        ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
have inr : ∀ (m : l ∈ ts.permutationsAux (t :: is)),
  (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Tactic: rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
have inl : (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
  is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
Tactic: subst e
Cleared hypotheses: l, e
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
is' : List α
p' : is' ~ t :: is
⊢ (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
have inl : ∀ (l₁ l₂ : List α) (e : is' = l₁ ++ t :: l₂),
  (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
Tactic: rcases append_of_mem (p'.symm.subset mem_cons_self) with ⟨l₁, l₂, e⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
⊢ (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
have inl : ∀ (p' : l₁ ++ t :: l₂ ~ t :: is),
  (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α), l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
Tactic: subst is'
Cleared hypotheses: is', p', e
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α), l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
have p : l₁ ++ l₂ ~ is
Tactic: have p := (perm_middle.symm.trans p').cons_inv
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α), l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
have inl : ∀ (p' : l₁ ++ [t] ~ t :: is) (p : l₁ ++ [] ~ is),
  (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts
Tactic: rcases l₂ with - | ⟨a, l₂'⟩
Cleared hypotheses: l₂, p', p
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
inl :
  ∀ (p' : l₁ ++ [t] ~ t :: is) (p : l₁ ++ [] ~ is),
    (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
      l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
        ∃ (l₁_1 : List α),
          ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α), l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
have inl₁ : ∀ (a : α) (l₂' : List α) (p' : l₁ ++ t :: a :: l₂' ~ t :: is) (p : l₁ ++ a :: l₂' ~ is),
  (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
Tactic: rcases l₂ with - | ⟨a, l₂'⟩
Cleared hypotheses: l₂, p', p
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b : α
l : List α
⊢ flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
have cons : ∀ (c : α) (l : List α)
  (ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)),
  flatMap (permutations'Aux b) (permutations'Aux a (c :: l)) ~
    flatMap (permutations'Aux a) (permutations'Aux b (c :: l))
Tactic: induction l with
  | nil => exact Perm.swap [a, b] [b, a] []
  | cons c l ih => ?_
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ flatMap (permutations'Aux b) (permutations'Aux a (c :: l)) ~
    flatMap (permutations'Aux a) (permutations'Aux b (c :: l))
have cons : (b :: a :: c :: l) ::
    (a :: b :: c :: l) ::
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l))) ~
  (a :: b :: c :: l) ::
    (b :: a :: c :: l) ::
      (map (cons b ∘ cons c) (permutations'Aux a l) ++
        flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l)))
Tactic: simp only [permutations'Aux, flatMap_cons, map_cons, map_map, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l)))
have cons : map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
  map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))
Tactic: apply Perm.swap'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (permutations'Aux b') (map (cons c) (permutations'Aux a' l)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
have simp : flatMap (fun (a : List α) ↦ (b' :: c :: a) :: map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
  map (cons b' ∘ cons c) (permutations'Aux a' l) ++ map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Tactic: simp only [flatMap_map, permutations'Aux]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun (a : List α) ↦ [b' :: c :: a] ++ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
have refine : HAppend.hAppend (α := List (List α)) (flatMap (fun (x : List α) ↦ [b' :: c :: x]) (permutations'Aux a' l))
    (flatMap (fun (a : List α) ↦ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l)) ~
  map (cons b' ∘ cons c) (permutations'Aux a' l) ++ map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Tactic: refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ HAppend.hAppend (α := List (List α)) (flatMap (fun (x : List α) ↦ [b' :: c :: x]) (permutations'Aux a' l))
      (flatMap (fun (a : List α) ↦ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
have rw : map (fun (x : List α) ↦ b' :: c :: x) (permutations'Aux a' l) ++
    map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l)) ~
  map (cons b' ∘ cons c) (permutations'Aux a' l) ++ map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Tactic: rw [← map_eq_flatMap, ← map_flatMap]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))
have this : ∀ (a b : α),
  flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
Tactic: have :
    ∀ a b,
      (map (cons c) (permutations'Aux a l)).flatMap (permutations'Aux b) ~
        map (cons b ∘ cons c) (permutations'Aux a l) ++
          map (cons c) ((permutations'Aux a l).flatMap (permutations'Aux b)) := by
    intro a' b'
    simp only [flatMap_map, permutations'Aux]
    change (permutations'Aux _ l).flatMap (fun a => ([b' :: c :: a] ++
      map (cons c) (permutations'Aux _ a))) ~ _
    refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_
    rw [← map_eq_flatMap, ← map_flatMap]
    exact Perm.refl _
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))
have cons : map (cons a ∘ cons c) (permutations'Aux b l) ++
    (map (cons b ∘ cons c) (permutations'Aux a l) ++
      map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))) ~
  map (cons b ∘ cons c) (permutations'Aux a l) ++
    (map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))
Tactic: refine (((this _ _).append_left _).trans ?_).trans ((this _ _).append_left _).symm
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++
      (map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))
have cons : map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons b ∘ cons c) (permutations'Aux a l) ++
    map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l)) ~
  map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons a ∘ cons c) (permutations'Aux b l) ++
    map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l))
Tactic: rw [← append_assoc, ← append_assoc]