-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem cons_subperm_of_not_mem_of_mem {a : α} {l₁ l₂ : List α} (h₁ : a ∉ l₁) (h₂ : a ∈ l₂)
    (s : l₁ <+~ l₂) : a :: l₁ <+~ l₂

Proof state:
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s'✝ : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ l₂✝
m : a ∈ l₂✝
t : List α
p' : t ~ a :: l₁
s' : t <+ l₂✝
⊢ a :: l₁ <+~ b :: l₂✝

Tactic:
exact ⟨t, p', s'.cons _⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
⊢ a ∈ r₂

Tactic:
simp only [find?, mem_cons] at h₂

Result:
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
h₂ : a = b ∨ a ∈ r₂
⊢ a ∈ r₂

Proof state:
case intro.intro.cons
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ l₂✝
⊢ a :: l₁ <+~ b :: l₂✝

Tactic:
match h₂ with
| .inl e => subst_vars; exact ⟨_ :: r₁, p.cons _, s'.cons₂ _⟩
| .inr m => let ⟨t, p', s'⟩ := ih h₁ m p; exact ⟨t, p', s'.cons _⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ l₂✝
e : a = b
⊢ a :: l₁ <+~ b :: l₂✝

Tactic:
subst_vars

Result:
α : Type u_1
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
l₁ : List α
p : r₁ ~ l₁
ih : ∀ {l₁ : List α}, ¬b ∈ l₁ → b ∈ l₂✝ → r₁ ~ l₁ → b :: l₁ <+~ l₂✝
h₁ : ¬b ∈ l₁
h₂ : b = b ∨ b ∈ l₂✝
⊢ b :: l₁ <+~ b :: l₂✝

Proof state:
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: l₁✝ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
⊢ t₁ ++ t₂ <+ t₁ ++ b :: t₂

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.cons₂
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
am : a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂

Tactic:
obtain ⟨t₁, t₂, rfl⟩ := append_of_mem bm

Result:
case intro.intro.cons₂.intro.intro
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: l₁✝ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂

Proof state:
case intro.intro.cons₂.intro.intro
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: l₁✝ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂

Tactic:
have st : t₁ ++ t₂ <+ t₁ ++ b :: t₂ := by simp

Result:
case intro.intro.cons₂.intro.intro
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: l₁✝ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
st : t₁ ++ t₂ <+ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂

Proof state:
case intro.intro.cons₂
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: l₁✝ ~ l₁
⊢ a :: l₁ <+~ b :: r₂

Tactic:
have bm : b ∈ l₁ := p.subset <| mem_cons_self _ _

Result:
case intro.intro.cons₂
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
⊢ a :: l₁ <+~ b :: r₂

Proof state:
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
h₂ : a = b ∨ a ∈ r₂
⊢ a ∈ r₂

Tactic:
exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm

Result:
no goals

Proof state:
case intro.intro.cons₂
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
⊢ a :: l₁ <+~ b :: r₂

Tactic:
have am : a ∈ r₂ := by
  simp only [find?, mem_cons] at h₂
  exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm

Result:
case intro.intro.cons₂
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: l₁✝ ~ l₁
bm : b ∈ l₁
am : a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂

Proof state:
case intro.intro.cons
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: l₂✝
p : r₁ ~ l₁
⊢ a :: l₁ <+~ b :: l₂✝

Tactic:
simp at h₂

Result:
case intro.intro.cons
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ l₂✝
⊢ a :: l₁ <+~ b :: l₂✝

Proof state:
case intro.intro.cons₂.intro.intro.intro.intro
α : Type u_1
a : α
l₂ l l₁✝ r₂ : List α
b : α
a✝ : l₁✝ <+ r₂
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ r₂ → l₁✝ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: l₁✝ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
st : t₁ ++ t₂ <+ t₁ ++ b :: t₂
t : List α
p' : t ~ a :: (t₁ ++ t₂)
s' : t <+ r₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂

Tactic:
exact ⟨b :: t, (p'.cons b).trans <| (swap ..).trans (perm_middle.symm.cons a), s'.cons₂ _⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ l₂✝
m : a ∈ l₂✝
⊢ a :: l₁ <+~ b :: l₂✝

Tactic:
let ⟨t, p', s'⟩ := ih h₁ m p

Result:
α : Type u_1
a : α
l₂ l r₁ l₂✝ : List α
b : α
s'✝ : r₁ <+ l₂✝
ih : ∀ {l₁ : List α}, ¬a ∈ l₁ → a ∈ l₂✝ → r₁ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ l₂✝
m : a ∈ l₂✝
t : List α
p' : t ~ a :: l₁
s' : t <+ l₂✝
⊢ a :: l₁ <+~ b :: l₂✝

Proof state:
α : Type u_1
l₂ l r₁ l₂✝ : List α
b : α
s' : r₁ <+ l₂✝
l₁ : List α
p : r₁ ~ l₁
ih : ∀ {l₁ : List α}, ¬b ∈ l₁ → b ∈ l₂✝ → r₁ ~ l₁ → b :: l₁ <+~ l₂✝
h₁ : ¬b ∈ l₁
h₂ : b = b ∨ b ∈ l₂✝
⊢ b :: l₁ <+~ b :: l₂✝

Tactic:
exact ⟨_ :: r₁, p.cons _, s'.cons₂ _⟩

Result:
no goals

Proof state:
case intro.intro.slnil
α : Type u_1
a : α
l₂ l l₁ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ []
p : [] ~ l₁
⊢ a :: l₁ <+~ []

Tactic:
cases h₂

Result:
no goals

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ l₂
s : l₁ <+~ l₂
⊢ a :: l₁ <+~ l₂

Tactic:
obtain ⟨l, p, s⟩ := s

Result:
case intro.intro
α : Type u_1
a : α
l₁ l₂ : List α
h₁ : ¬a ∈ l₁
h₂ : a ∈ l₂
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ a :: l₁ <+~ l₂