α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t
refine' ⟨_, fun h => le_trans h <| le_cons_self _ _⟩
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t
suffices ∀ {t'} (_ : s ≤ t') (_ : a ∈ t'), a ::ₘ s ≤ t' by
  exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
introv h
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ¬a ∈ s → a ∈ t' → a ::ₘ s ≤ t'
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'
revert m
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ¬a ∈ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ¬a ∈ s → a ∈ t' → a ::ₘ s ≤ t'
refine' leInductionOn h _
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ ↑l₁
m₂ : a ∈ ↑l₂
⊢ a ::ₘ ↑l₁ ≤ ↑l₂
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ¬a ∈ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂
introv s m₁ m₂
case intro.intro
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ : List α
m₁ : ¬a ∈ ↑l₁
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ ↑(r₁ ++ a :: r₂)
⊢ a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ ↑l₁
m₂ : a ∈ ↑l₂
⊢ a ::ₘ ↑l₁ ≤ ↑l₂
rcases mem_split m₂ with ⟨r₁, r₂, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ : List α
m₁ : ¬a ∈ ↑l₁
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ ↑(r₁ ++ a :: r₂)
⊢ a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)
exact
  perm_middle.subperm_left.2
    ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)
no goals
α : Type u_1
β : Type ?u.36383
γ : Type ?u.36386
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t
exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))