-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Nodup.perm_iff_eq_of_sublist {l₁ l₂ l : List α} (d : Nodup l)
    (s₁ : l₁ <+ l) (s₂ : l₂ <+ l) : l₁ ~ l₂ ↔ l₁ = l₂

Proof state:
case slnil
α : Type u_1
l₂ l l₁ : List α
s₁ : l₁ <+ []
h : l₁ ~ []
d : True
⊢ l₁ = []

Tactic:
exact h.eq_nil

Result:
no goals

Proof state:
case cons₂
α : Type u_1
l₂ l l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝ → l₁ = l₁✝
l₁ : List α
s₁ : l₁ <+ a :: l₂✝
h : l₁ ~ a :: l₁✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
⊢ l₁ = a :: l₁✝

Tactic:
match s₁ with
| .cons _ s₁ =>
  have := Subperm.subset ⟨_, h, s₁⟩ (.head _)
  exact (d.1 this).elim
| .cons₂ _ s₁ => rw [IH d.2 s₁ h.cons_inv]

Result:
no goals

Proof state:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
s₂ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁✝ : List α
s₁✝ : l₁✝ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁ : List α
s₁ : l₁ <+ l₂✝
h : l₁ ~ l₁✝¹
⊢ l₁ = l₁✝¹

Tactic:
exact IH d.2 s₁ h

Result:
no goals

Proof state:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
s₂ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁ : List α
s₁✝ : l₁ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁✝ : List α
s₁ : l₁✝ <+ l₂✝
h : a :: l₁✝ ~ l₁✝¹
this : a ∈ l₂✝
⊢ a :: l₁✝ = l₁✝¹

Tactic:
exact (d.1 this).elim

Result:
no goals

Proof state:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
a✝ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁ : List α
s₁✝ : l₁ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁✝ : List α
s₁ : l₁✝ <+ l₂✝
h : a :: l₁✝ ~ a :: l₁✝¹
⊢ a :: l₁✝ = a :: l₁✝¹

Tactic:
rw [IH d.2 s₁ h.cons_inv]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l : List α
d : l.Nodup
s₁ : l₁ <+ l
s₂ : l₂ <+ l
h : l₁ = l₂
⊢ l₁ ~ l₂

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
a✝ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁✝ : List α
s₁✝ : l₁✝ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁ : List α
s₁ : l₁ <+ l₂✝
h : l₁ ~ a :: l₁✝¹
this : a ∈ l₂✝
⊢ l₁ = a :: l₁✝¹

Tactic:
exact (d.1 this).elim

Result:
no goals

Proof state:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
s₂ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁ : List α
s₁✝ : l₁ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁✝ : List α
s₁ : l₁✝ <+ l₂✝
h : a :: l₁✝ ~ l₁✝¹
⊢ a :: l₁✝ = l₁✝¹

Tactic:
have := Subperm.subset ⟨_, h.symm, s₂⟩ (.head _)

Result:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
s₂ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁ : List α
s₁✝ : l₁ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁✝ : List α
s₁ : l₁✝ <+ l₂✝
h : a :: l₁✝ ~ l₁✝¹
this : a ∈ l₂✝
⊢ a :: l₁✝ = l₁✝¹

Proof state:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
a✝ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁✝ : List α
s₁✝ : l₁✝ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁ : List α
s₁ : l₁ <+ l₂✝
h : l₁ ~ a :: l₁✝¹
⊢ l₁ = a :: l₁✝¹

Tactic:
have := Subperm.subset ⟨_, h, s₁⟩ (.head _)

Result:
α : Type u_1
l₂ l l₁✝¹ l₂✝ : List α
a : α
a✝ : l₁✝¹ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝¹ → l₁ = l₁✝¹
l₁✝ : List α
s₁✝ : l₁✝ <+ a :: l₂✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
l₁ : List α
s₁ : l₁ <+ l₂✝
h : l₁ ~ a :: l₁✝¹
this : a ∈ l₂✝
⊢ l₁ = a :: l₁✝¹

Proof state:
case cons
α : Type u_1
l₂ l l₁✝ l₂✝ : List α
a : α
s₂ : l₁✝ <+ l₂✝
IH : ∀ {l₁ : List α}, l₂✝.Nodup → l₁ <+ l₂✝ → l₁ ~ l₁✝ → l₁ = l₁✝
l₁ : List α
s₁ : l₁ <+ a :: l₂✝
h : l₁ ~ l₁✝
d : ¬a ∈ l₂✝ ∧ Pairwise (fun x1 x2 => ¬x1 = x2) l₂✝
⊢ l₁ = l₁✝

Tactic:
match s₁ with
| .cons _ s₁ => exact IH d.2 s₁ h
| .cons₂ _ s₁ =>
  have := Subperm.subset ⟨_, h.symm, s₂⟩ (.head _)
  exact (d.1 this).elim

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l : List α
d : l.Nodup
s₁ : l₁ <+ l
s₂ : l₂ <+ l
h : l₁ ~ l₂
⊢ l₁ = l₂

Tactic:
induction s₂ generalizing l₁ with simp [Nodup, List.forall_mem_ne] at d
| slnil => exact h.eq_nil
| cons a s₂ IH =>
  match s₁ with
  | .cons _ s₁ => exact IH d.2 s₁ h
  | .cons₂ _ s₁ =>
    have := Subperm.subset ⟨_, h.symm, s₂⟩ (.head _)
    exact (d.1 this).elim
| cons₂ a _ IH =>
  match s₁ with
  | .cons _ s₁ =>
    have := Subperm.subset ⟨_, h, s₁⟩ (.head _)
    exact (d.1 this).elim
  | .cons₂ _ s₁ => rw [IH d.2 s₁ h.cons_inv]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l : List α
d : l.Nodup
s₁ : l₁ <+ l
s₂ : l₂ <+ l
⊢ l₁ ~ l₂ ↔ l₁ = l₂

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h]⟩

Result:
α : Type u_1
l₁ l₂ l : List α
d : l.Nodup
s₁ : l₁ <+ l
s₂ : l₂ <+ l
h : l₁ ~ l₂
⊢ l₁ = l₂