α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
⊢ ∀ (x_1 : α), x_1 ∈ x :: l₁ → count x_1 (x :: l₁) ≤ count x_1 l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <+~ l₂
x : α
hx : count x l₁ < count x l₂
⊢ x :: l₁ <+~ l₂
rw [subperm_ext_iff] at h⊢
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
⊢ count y (x :: l₁) ≤ count y l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
⊢ ∀ (x_1 : α), x_1 ∈ x :: l₁ → count x_1 (x :: l₁) ≤ count x_1 l₂
intro y hy
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : y = x
⊢ count y (x :: l₁) ≤ count y l₂

case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y (x :: l₁) ≤ count y l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
⊢ count y (x :: l₁) ≤ count y l₂
by_cases hy' : y = x
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
y : α
hx : count y l₁ < count y l₂
hy : y ∈ y :: l₁
⊢ count y (y :: l₁) ≤ count y l₂
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : y = x
⊢ count y (x :: l₁) ≤ count y l₂
subst x
no goals
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
y : α
hx : count y l₁ < count y l₂
hy : y ∈ y :: l₁
⊢ count y (y :: l₁) ≤ count y l₂
simpa using Nat.succ_le_of_lt hx
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y l₁ ≤ count y l₂
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y (x :: l₁) ≤ count y l₂
rw [count_cons_of_ne hy']
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ y ∈ l₁
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ count y l₁ ≤ count y l₂
refine' h y _
no goals
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h✝ : l₁ <+~ l₂
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
x : α
hx : count x l₁ < count x l₂
y : α
hy : y ∈ x :: l₁
hy' : ¬y = x
⊢ y ∈ l₁
simpa [hy'] using hy